Inference at * 1 
Iof proof for Lemma member nth tl:

.....basecase..... NILNIL

1. T : Type
  x:T, L:(T List). (x  nth_tl(0;L))  (x  L) 

latex

 by ((Reduce 0) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	i z j, i <z j, P  Q, (x  l), x:A. B(x), x:AB(x), Type, s = t, type List, t  T
Lemmas	l member wf